$X$ is finite
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$finite{-}type(\{$p$::Id $\times$ Knd$\mid$ $\exists$$e$:E. (loc($e$) = ($p$.1) \& kind($e$) = ($p$.2) \& ($\uparrow$($e$ $\in_{b}$ $X$)))\} )